Conservativity theorem

In mathematical logic, the conservativity theorem states the following: Suppose that a closed formula

[math]\displaystyle{ \exists x_1\ldots\exists x_m\,\varphi(x_1,\ldots,x_m) }[/math]

is a theorem of a first-order theory [math]\displaystyle{ T }[/math]. Let [math]\displaystyle{ T_1 }[/math] be a theory obtained from [math]\displaystyle{ T }[/math] by extending its language with new constants

[math]\displaystyle{ a_1,\ldots,a_m }[/math]

and adding a new axiom

[math]\displaystyle{ \varphi(a_1,\ldots,a_m) }[/math].

Then [math]\displaystyle{ T_1 }[/math] is a conservative extension of [math]\displaystyle{ T }[/math], which means that the theory [math]\displaystyle{ T_1 }[/math] has the same set of theorems in the original language (i.e., without constants [math]\displaystyle{ a_i }[/math]) as the theory [math]\displaystyle{ T }[/math].

In a more general setting, the conservativity theorem is formulated for extensions of a first-order theory by introducing a new functional symbol:

Suppose that a closed formula [math]\displaystyle{ \forall \vec{y}\,\exists x\,\!\,\varphi(x,\vec{y}) }[/math] is a theorem of a first-order theory [math]\displaystyle{ T }[/math], where we denote [math]\displaystyle{ \vec{y}:=(y_1,\ldots,y_n) }[/math]. Let [math]\displaystyle{ T_1 }[/math] be a theory obtained from [math]\displaystyle{ T }[/math] by extending its language with a new functional symbol [math]\displaystyle{ f }[/math] (of arity [math]\displaystyle{ n }[/math]) and adding a new axiom [math]\displaystyle{ \forall \vec{y}\,\varphi(f(\vec{y}),\vec{y}) }[/math]. Then [math]\displaystyle{ T_1 }[/math] is a conservative extension of [math]\displaystyle{ T }[/math], i.e. the theories [math]\displaystyle{ T }[/math] and [math]\displaystyle{ T_1 }[/math] prove the same theorems not involving the functional symbol [math]\displaystyle{ f }[/math]).

References

• Elliott Mendelson (1997). Introduction to Mathematical Logic (4th ed.) Chapman & Hall.
• J.R. Shoenfield (1967). Mathematical Logic. Addison-Wesley Publishing Company.